Nuprl Lemma : ma-has-effect_wf 0,22

A:MsgA, k:Knd. ma-has-effect(A;k Prop 
latex


DefinitionsKnd, t  T, Id, x:AB(x), xt(x), 1of(t), map(f;as), KindDeq, deq-member(eq;x;L), b, Prop, a:A fp B(a), ma-has-effect(M;k), MsgA
Lemmasmsga wf, assert wf, deq-member wf, Kind-deq wf, map wf, pi1 wf, Id wf, Knd wf

origin